/******************************************************************************

    Copyright (C) 2006 - 2010 Alessio Stalla (alessiostalla@gmail.com)

    This file is part of PrettyProlog.

    PrettyProlog is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    PrettyProlog is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with PrettyProlog; if not, write to the Free Software
    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA

    See the file COPYING for further details.

 *****************************************************************************/

package prettyprolog.engine;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;

import prettyprolog.datatypes.Callable;
import prettyprolog.datatypes.Substitution;
import prettyprolog.datatypes.Symbol;
import prettyprolog.datatypes.Term;
import prettyprolog.engine.listeners.TheoryEvent;
import prettyprolog.engine.listeners.TheoryListener;
import prettyprolog.engine.syspreds.SystemPredicate;

/**
 * A Theory is an ordered collection of Clauses. You can assign listeners to a
 * Theory to get notified of the insertion, deletion, and selection of a Clause.
 */
public class Theory {

	/**
	 * List of clauses that constitute the Theory.
	 */
	protected List<Clause> clauses = new ArrayList<Clause>();
	/**
	 * The engine used to evaluate directives at assertion time
	 */
	protected Engine engine;
	/**
	 * Associations between symbols and functions
	 */
	protected Map<Symbol, Function> functions = new HashMap<Symbol, Function>();
	
	public Theory(Engine engine) {
		this.engine = engine;
	}

	/**
	 * Instances of this class hold the information returned by the nextClause()
	 * method, i.e. clause, substitution, index, and clause string. See the
	 * fields and methods for more info.
	 */
	public static class ClauseInfo {

		/** A copy of the clause whose head unifies with the given term */
		protected Clause renamed_clause;
		/** The substitution that unifies the term and the clause's head */
		protected Substitution subst;
		/** The position of the clause in the theory */
		protected int index;
		/**
		 * The "original" clause, without variables renamed
		 */
		protected Clause clause;

		public Clause getRenamedClause() {
			return renamed_clause;
		}

		public Substitution getSubstitution() {
			return subst;
		}

		public int getIndex() {
			return index;
		}

		public Clause getClause() {
			return clause;
		}
	}

	/**
	 * This method is used by the Engine to select which Clause to use in the
	 * solving process. When it succeeds finding a Clause, it generates a
	 * clauseSelected event.
	 * 
	 * @param t
	 *            a Term which must unify with the selected Clause's head.
	 * @param u
	 *            the UnificationAlgorithm used to perform unifications.
	 * @param i
	 *            the index (inclusive) from which to start the search.
	 * @return the next clause whose head unifies with t, the substitution
	 *         resulting from such unification, and the index at which the
	 *         engine should continue searching for next clauses.
	 */
	public ClauseInfo nextClause(Term t, UnificationAlgorithm u, int i) {
		ClauseInfo info = new ClauseInfo();
		int sz = clauses.size();
		for (int j = i; j < sz; j++) {
			Clause nxt = clauses.get(j);
			Clause copy = nxt.copy();
			Substitution s = u.unify(t, copy.getHead());
			if (s != null) {
				info.renamed_clause = copy;
				info.subst = s;
				info.index = j;
				info.clause = nxt;
				dispatchSelectEvent(nxt, j);
				return info;
			}
		}
		return null;
	}

	/**
	 * Adds c at the position i in the theory, and notifies all the listeners.
	 */
	public void assertClause(Clause c, int i) {
		if(c.isDirective()) {
			if(engine == null) {
				throw new IllegalStateException("This Theory cannot execute directives because it has no associated Engine: " + this);
			}
			for(Term t : c.getBody().getArgs()) {
				if(t instanceof Callable) {
					Callable callable = (Callable) t;
					SystemPredicate p = systemPredicate(callable);
					if(p != null) {
						p.call(engine, new Substitution(), callable.getArgs());
					} else {
						throw new IllegalArgumentException("Cannot execute directive " + c + " because " + t + " is not a system predicate");			
					}
				} 
			}
			clauses.add(i, c);
			dispatchAssertEvent(c, i);
		} else if(systemPredicate(c) == null) {
			clauses.add(i, c);
			dispatchAssertEvent(c, i);
		} else {
			throw new IllegalArgumentException("Cannot assert " + c + " because it's a system predicate");
		}
	}

	/**
	 * Adds c at the end of the theory, and notifies all the listeners.
	 */
	public void assertz(Clause c) {
		assertClause(c, clauses.size());
	}

	/**
	 * Adds c at the beginning of the theory, and notifies all the listeners.
	 */
	public void asserta(Clause c) {
		assertClause(c, 0);
	}

	/**
	 * Removes c from the theory, if it's present, and notifies all the
	 * listeners.
	 * 
	 * @return the removed clause, or null if the theory didn't contain such a
	 *         clause
	 */
	public Clause retract(Clause c) {
		if (clauses.remove(c)) {
			dispatchRetractEvent(c, 0);
			return c;
		} else {
			return null;
		}
	}

	/**
	 * Convenience method for loading theories.<br />
	 * Asserts all the clauses of th into this theory.
	 */
	public void assertAll(Theory th) {
		for(Map.Entry<Symbol, SystemPredicate> e : th.systemPredicates.entrySet()) {
			systemPredicates.put(e.getKey(), e.getValue());
		}
		Iterator<Clause> it = th.clauses.iterator();
		while (it.hasNext()) {
			assertz(it.next());
		}
	}

	/** Removes every Clause from this Theory. */
	public void retractAll() {
		while (!clauses.isEmpty()) {
			dispatchRetractEvent(clauses.remove(0), 0);
		}
	}
	
	/** Removes every Clause and every system predicate from this Theory. */
	public void clear() {
		retractAll();
		systemPredicates.clear();
	}

	/** @return the clause at index i (zero-based). */
	public Clause getClause(int i) {
		return clauses.get(i);
	}

	/** @return the number of clauses contained in this theory */
	public int size() {
		return clauses.size();
	}

	/** @return an iterator that cycles through the clauses of this theory. */
	public Iterator<Clause> iterator() {
		return new Iterator<Clause>() {

			private Iterator<Clause> it = clauses.iterator();

			public Clause next() {
				return it.next();
			}

			public boolean hasNext() {
				return it.hasNext();
			}

			public void remove() {
				throw new UnsupportedOperationException();
			}

		};
	}

	// LISTENERS
	/** The List of listeners associated with this Theory. */
	protected List<TheoryListener> listeners = new LinkedList<TheoryListener>();

	/** Associates a listener to this Theory. */
	public void addTheoryListener(TheoryListener l) {
		listeners.add(l);
	}

	/**
	 * Removes a listener from those associated to this Theory.
	 * 
	 * @return <code>true</code> if the listener was present in the list,
	 *         <code>false</code> otherwise.
	 */
	public boolean removeTheoryListener(TheoryListener l) {
		return listeners.remove(l);
	}

	/** Notifies every listener that a Clause has been asserted. */
	protected void dispatchAssertEvent(Clause c, int i) {
		TheoryEvent ev = new TheoryEvent(c, i);
		for (TheoryListener listener : listeners)
			listener.clauseAsserted(ev);
	}

	/** Notifies every listener that a Clause has been retracted. */
	protected void dispatchRetractEvent(Clause c, int i) {
		TheoryEvent ev = new TheoryEvent(c, i);
		for (TheoryListener listener : listeners)
			listener.clauseRetracted(ev);
	}

	/** Notifies every listener that a Clause has been selected. */
	protected void dispatchSelectEvent(Clause c, int i) {
		TheoryEvent ev = new TheoryEvent(c, i);
		for (TheoryListener listener : listeners)
			listener.clauseSelected(ev);
	}

	// END LISTENERS

	/**
	 * Makes a copy of this theory which has the same clauses, but not the
	 * listeners attached to this Theory.
	 */
	public Theory copy() {
		Theory copy = new Theory(engine);
		copy.clauses = new ArrayList<Clause>(clauses);
		copy.systemPredicates = new HashMap<Symbol, SystemPredicate>(systemPredicates);
		return copy;
	}
	
	// System predicates
	private Map<Symbol, SystemPredicate> systemPredicates = new HashMap<Symbol, SystemPredicate>();

	/**
	 * Registers a System Predicate with the given Symbol. Note that currently
	 * the engine doesn't check that a syspred is called with the right number
	 * of parameters, nor that the Theory doesn't contain clauses that are
	 * shadowed by system predicates.
	 * 
	 * @param sym
	 *            the Symbol identifying the system predicate. For example, if
	 *            the syspred is foo/3, sym will be "foo".
	 * @param s
	 *            the SystemPredicate object whose call() method will be invoked to
	 *            resolve the effect of the syspred.
	 */
	public void registerSystemPredicate(Symbol sym, SystemPredicate s) {
		systemPredicates.put(sym, s);
	}

	/** Removes the system predicate associated with <code>sym</code>. */
	public void removeSystemPredicate(Symbol sym) {
		systemPredicates.remove(sym);
	}
	
	public SystemPredicate systemPredicate(Callable c) {
		return systemPredicate(c.getSymbol(), c.getArgCount());
	}

	public SystemPredicate systemPredicate(Clause c) {
		return systemPredicate(c.getHead());
	}
	
	/** @return the System Predicate corresponding to <code>sym</code>. */
	public SystemPredicate systemPredicate(Symbol sym, int nargs) {
		SystemPredicate s = systemPredicates.get(sym);
		if(s != null && s.getRequiredArgumentsCount() == nargs) {
			return s;
		} else {
			return null;
		}
	}

	//End System Predicates
	
	public Function getFunction(Symbol s) {
		return functions.get(s);
	}
	
	public Function setFunction(Symbol s, Function f) {
		return functions.put(s, f);
	}

	/** @return a printed representation of this theory. */
	public String toString() {
		String nl = System.getProperty("line.separator", "\n");
		String str = "PrettyProlog theory:" + nl;
		for (Clause c : clauses) {
			str += "  " + c + nl;
		}
		return str;
	}
}